(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |

   The benchmark encodes 2 simple processors
   receiving instructions to decode and execute.
   The processors compute the same function on 2 operands but
   their decoding units differ in the way they
   communicate the result.
   We check that, modulo reinterpretation of the
   decoded instructions, the result is the same.
   We added a "mode" flag to force the decoding
   unit to return the result in two different ways.

   The encoded design is a modification of Example 11.2, at page 20 of
   "Introduction to Verilog", by Peter M. Nyasulu
   available online.

   Generated by Roberto Bruttomesso <roberto.bruttomesso@gmail.com>

|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun opcode () (_ BitVec 8))
(declare-fun operator1 () (_ BitVec 8))
(declare-fun opr1_1 () (_ BitVec 8))
(declare-fun op1_1 () (_ BitVec 8))
(declare-fun opr1_2 () (_ BitVec 8))
(declare-fun op1_2 () (_ BitVec 8))
(declare-fun operator2 () (_ BitVec 8))
(declare-fun opr2_1 () (_ BitVec 8))
(declare-fun op2_1 () (_ BitVec 8))
(declare-fun opr2_2 () (_ BitVec 8))
(declare-fun op2_2 () (_ BitVec 8))
(declare-fun decode_1 () (_ BitVec 17))
(declare-fun dec_func_1 () (_ BitVec 1))
(declare-fun deci_func_1 () (_ BitVec 1))
(declare-fun func_1 () (_ BitVec 1))
(declare-fun out_1 () (_ BitVec 8))
(declare-fun mode_1 () (_ BitVec 1))
(declare-fun decode_2 () (_ BitVec 17))
(declare-fun dec_func_2 () (_ BitVec 1))
(declare-fun deci_func_2 () (_ BitVec 1))
(declare-fun func_2 () (_ BitVec 1))
(declare-fun out_2 () (_ BitVec 8))
(declare-fun mode_2 () (_ BitVec 1))
(assert (let ((?v_4 (= opr1_1 operator1)) (?v_5 (= opcode (_ bv136 8))) (?v_1 (= dec_func_1 (_ bv1 1))) (?v_0 (= opr2_1 operator2)) (?v_6 (= opcode (_ bv137 8))) (?v_2 (= dec_func_1 (_ bv0 1))) (?v_7 (= opcode (_ bv138 8))) (?v_3 (= opr2_1 (_ bv1 8))) (?v_8 (= deci_func_1 (_ bv1 1))) (?v_9 (= deci_func_1 (_ bv0 1))) (?v_10 (= mode_1 (_ bv0 1))) (?v_11 (= func_1 ((_ extract 16 16) decode_1))) (?v_12 ((_ extract 15 8) decode_1)) (?v_13 ((_ extract 7 0) decode_1)) (?v_18 (= opr1_2 operator1)) (?v_15 (= dec_func_2 (_ bv1 1))) (?v_14 (= opr2_2 operator2)) (?v_16 (= dec_func_2 (_ bv0 1))) (?v_17 (= opr2_2 (_ bv1 8))) (?v_19 (= deci_func_2 (_ bv1 1))) (?v_20 (= deci_func_2 (_ bv0 1))) (?v_21 (= mode_2 (_ bv0 1))) (?v_22 ((_ extract 16 9) decode_2)) (?v_23 (= func_2 ((_ extract 8 8) decode_2))) (?v_24 ((_ extract 7 0) decode_2))) (and ?v_4 (ite ?v_5 (and ?v_1 ?v_0) (ite ?v_6 (and ?v_2 ?v_0) (ite ?v_7 (and ?v_1 ?v_3) (and ?v_2 ?v_3)))) ?v_4 (ite ?v_5 (and ?v_8 ?v_0) (ite ?v_6 (and ?v_9 ?v_0) (ite ?v_7 (and ?v_8 ?v_3) (and ?v_9 ?v_3)))) (ite ?v_10 (= decode_1 (concat (concat dec_func_1 opr1_1) opr2_1)) (= decode_1 (concat (concat deci_func_1 opr2_1) opr1_1))) (ite ?v_10 (and ?v_11 (= op1_1 ?v_12) (= op2_1 ?v_13)) (and ?v_11 (= op2_1 ?v_12) (= op1_1 ?v_13))) (ite (= func_1 (_ bv1 1)) (= out_1 (bvadd op1_1 op2_1)) (= out_1 (bvor op1_1 op2_1))) ?v_18 (ite ?v_5 (and ?v_15 ?v_14) (ite ?v_6 (and ?v_16 ?v_14) (ite ?v_7 (and ?v_15 ?v_17) (and ?v_16 ?v_17)))) ?v_18 (ite ?v_5 (and ?v_19 ?v_14) (ite ?v_6 (and ?v_20 ?v_14) (ite ?v_7 (and ?v_19 ?v_17) (and ?v_20 ?v_17)))) (ite ?v_21 (= decode_2 (concat (concat opr1_2 dec_func_2) opr2_2)) (= decode_2 (concat (concat opr2_2 deci_func_2) opr1_2))) (ite ?v_21 (and (= op1_2 ?v_22) ?v_23 (= op2_2 ?v_24)) (and (= op2_2 ?v_22) ?v_23 (= op1_2 ?v_24))) (ite (= func_2 (_ bv1 1)) (= out_2 (bvadd op1_2 op2_2)) (= out_2 (bvor op1_2 op2_2))) (= mode_1 mode_2) (not (= out_1 out_2)))))
(check-sat)
(exit)
